Inference at * 1 1 1 1 1 
Iof proof for Lemma fseg extend:



1. T : Type
2. l1 : T List
3. v : T
4. l2 : T List
5. L : T List
6. l2 = (L @ l1)
7. ||l1|| < ||l2||
8. l2[(||l2|| - (||l1||+1))] = v
9. (null(L))
10. L' : T List
11. L = (L' @ [last(L)])
12. 0 < ||L||
  last(L) = L[((||L||+||l1||) - (||l1||+1))] 

latex

 by ((((Unfold `last` ( 0)) 
CollapseTHEN (EqCD))) 
CollapseTHEN (Auto')) 

latex

C.

Definitions	last(L), l[i], , x:A. B(x), P  Q, x:AB(x), T, True, t  T, A, s = t, type List, Type, P & Q, x:A  B(x), A  B, a < b
Lemmas	le wf, squash wf, select wf